1. Field of the Invention
The invention relates to a method for the comparison of technical systems to check functional equivalence by means of system replacements.
2. Description of Related Art
As is known, even minor internal behaviour differences can easily lead to failure in the comparison of technical systems, in particular if large and complex systems are concerned.
In the case of such larger technical systems as, for instance, Application Specific Integrated Circuits (ASICs), at present there is no durable and satisfactory method of solving this problem.
Depending on the particular scope of application, there are a few known ideas to solve this problem.
A possible scenario, in which the above problem can occur, is implementation verification, when the synthesis results are to be compared to the synthesis inputs, in order to ensure that the synthesis process has not introduced any modifications into the functionality of the synthesis inputs.
Here especially the handling of so-called “library cells”, which serve as a simple way to illustrate the synthesis result, has shown to be problematic. Here, a large degree of freedom exists for modelling the internal behaviour of the library cells.
A popular method now consists of modifying the internal logic based on heuristics and in particular encoding of the internal states of the library cells so that the internal behaviour of the parts representing the library cell is exactly evident from the synthesis inputs.
Since these techniques work without knowledge of the synthesis inputs exclusively on the library cells and due to the extraordinarily large number of possible uses of library cells it is hardly to be avoided that this procedure is incomplete and error-prone.
Suitable modelling of library cells, however, is the basic pre-requisite for successful implementation verification.
An example of a known solution is FormalPro (™) software, an implementation verification tool developed by the firm Mentor Graphics. This uses heuristics, in order to deal with various problem scenarios in regard to library cells (see in this connection Hughes, Roger B.: Whole design formal verification of a 5-million gate design by equivalence checking is possible with a small memory footprint, DesignCon2000, February 2000).
Essentially, as a result of this idea, an attempt is made to find a standard format to illustrate the library cells. This solution moreover supports the aforementioned statement, according to which library cells represent a special problem.
The solution proposed by the invention overcomes these fundamental problems and can be used in numerous application scenarios.